

\begin{figure*}
\begin{center}
\begin{tikzpicture}[scale=1]
 \coordinate (bad1) at  (0,0){};
 \coordinate (bad2) at  ([shift={(-90pt,5pt)}]bad1){};
 \coordinate (bad3) at  ([shift={(-90pt,5pt)}]bad2){};
 \coordinate (bad4) at  ([shift={(-90pt,5pt)}]bad3){};
%
 \begin{scope} %% Scoping to make the clipping local
   \clip (bad1) ++(-30pt,75pt) parabola[bend pos=0.5] bend (bad1) ++(60pt,0pt) -- cycle;
   %% The upward closed set with fuzzy wave at the top
   \fill[para=red!80!white] (bad1) ++(-30pt,75pt) parabola[bend pos=0.5] bend (bad1) ++(60pt,0pt) -- cycle;
   \fill[white,fuzzywave] (bad1) ++(-40pt,60pt) rectangle +(80pt,40pt);
   \draw[red] (bad1) ++(-30pt,75pt) parabola[bend pos=0.5] bend (bad1) ++(60pt,0pt);
   %% Name
   \node[circle] at ($ (bad1)+(0pt,20pt) $){\tiny{$\phi_0=Bad$}};
   %% Une grosse patate
   \node[ellipse,fuzzywave,minimum height=40pt,minimum width=20pt,rotate=0, fill=blue!50!gray,opacity=0.5] at ($ (bad1)+(-45pt,35pt)+{(1)/2}*(10pt,10pt) $){};
 \end{scope}
%
 %% Repeating the potato, to create the illusion of intersection
 \node[ellipse,fuzzywave,minimum height=40pt,minimum width=20pt,rotate=0,draw=blue!50!gray] at ($ (bad1)+(-45pt,35pt)+{(1)/2}*(10pt,10pt) $){};
 \node[anchor=south west,scale=0.55] at ($ (bad1)+(-55pt,35pt)+{(1)/2}*(10pt,14pt)$) {$i_3$};
 % \draw[forward,->] ($ (bad2)+(-20pt,40pt) $) to ($ (bad1)+(-40pt,30pt)+(10pt,10pt) $) node[transitionLabel] {$post(i_2\wedge\phi_1)$};
%
%
 \begin{scope} %% Scoping to make the clipping local
   \clip (bad2) ++(-30pt,75pt) parabola[bend pos=0.5] bend (bad2) ++(60pt,0pt) -- cycle;
   %% The upward closed set with fuzzy wave at the top
   \fill[para=red!80!white] (bad2) ++(-30pt,75pt) parabola[bend pos=0.5] bend (bad2) ++(60pt,0pt) -- cycle;
   \fill[white,fuzzywave] (bad2) ++(-40pt,60pt) rectangle +(80pt,40pt);
   \draw[red] (bad2) ++(-30pt,75pt) parabola[bend pos=0.5] bend (bad2) ++(60pt,0pt);
   %% Name
   \node[circle] at ($ (bad2)+(0pt,20pt) $){\tiny{$\phi_1$}};
   % % Une grosse patate
   \node[ellipse,fuzzywave,minimum height=45pt,minimum width=25pt,rotate=50, fill=blue!50!gray,opacity=0.5] at ($ (bad2)+(-45pt,35pt)+{(2)/2}*(10pt,10pt) $){};
 \end{scope}
 \draw [->,thick, decorate, decoration={snake,amplitude=0.5mm,post length=2mm}] (bad1) --(bad2);
 %% Repeating the potato, to create the illusion of intersection
 \node[ellipse,fuzzywave,minimum height=45pt,minimum width=25pt,rotate=50,draw=blue!50!gray] at ($ (bad2)+(-45pt,35pt)+{(2)/2}*(10pt,10pt) $){};
 \node[anchor=south west,scale=0.55] at ($ (bad2)+(-55pt,35pt)+{(2)/2}*(10pt,14pt)$) {$i_2$};
%
 \begin{scope} %% Scoping to make the clipping local
   \clip (bad3) ++(-30pt,75pt) parabola[bend pos=0.5] bend (bad3) ++(60pt,0pt) -- cycle;
   %% The upward closed set with fuzzy wave at the top
   \fill[para=red!80!white] (bad3) ++(-30pt,75pt) parabola[bend pos=0.5] bend (bad3) ++(60pt,0pt) -- cycle;
   \fill[white,fuzzywave] (bad3) ++(-40pt,60pt) rectangle +(80pt,40pt);
   \draw[red] (bad3) ++(-30pt,75pt) parabola[bend pos=0.5] bend (bad3) ++(60pt,0pt);
   %% Name
   \node[circle] at ($ (bad3)+(0pt,20pt) $){\tiny{$\phi_2$}};
   % % Une grosse patate
   \node[ellipse,fuzzywave,minimum height=40pt,minimum width=20pt,rotate=35, fill=blue!50!gray,opacity=0.5] at ($ (bad3)+(-45pt,35pt)+{(3)/2}*(10pt,10pt) $){};
 \end{scope}
 \draw [->,thick, decorate, decoration={snake,amplitude=0.5mm,post length=2mm}] (bad2) --(bad3);
 %% Repeating the potato, to create the illusion of intersection
 \node[ellipse,fuzzywave,minimum height=40pt,minimum width=20pt,rotate=35,draw=blue!50!gray] at ($ (bad3)+(-45pt,35pt)+{(3)/2}*(10pt,10pt) $){};
 \node[anchor=south west,scale=0.55] at ($ (bad3)+(-55pt,35pt)+{(3)/2}*(10pt,14pt)$) {$i_1$};
%
 \begin{scope} %% Scoping to make the clipping local
   \clip (bad4) ++(-30pt,75pt) parabola[bend pos=0.5] bend (bad4) ++(60pt,0pt) -- cycle;
   %% The upward closed set with fuzzy wave at the top
   \fill[para=red!80!white] (bad4) ++(-30pt,75pt) parabola[bend pos=0.5] bend (bad4) ++(60pt,0pt) -- cycle;
   \fill[white,fuzzywave] (bad4) ++(-40pt,60pt) rectangle +(80pt,40pt);
   \draw[red] (bad4) ++(-30pt,75pt) parabola[bend pos=0.5] bend (bad4) ++(60pt,0pt);
   %% Name
   \node[circle] at ($ (bad4)+(0pt,20pt) $){\tiny{$\phi_3$}};
   % % Une grosse patate
   \node[ellipse,fuzzywave,minimum height=40pt,minimum width=20pt,rotate=90, fill=blue!50!gray,opacity=0.5] at ($ (bad4)+(-45pt,35pt)+{(4)/2}*(10pt,10pt) $){};
  \end{scope}
  \draw [->,thick, decorate, decoration={snake,amplitude=0.5mm,post length=2mm}] (bad3) --(bad4);
  %% Repeating the potato, to create the illusion of intersection
  \node[ellipse,fuzzywave,minimum height=40pt,minimum width=20pt,rotate=90,draw=blue!50!gray] at ($ (bad4)+(-45pt,35pt)+{(4)/2}*(10pt,10pt) $){};
  \node[anchor=south west,scale=0.55] at ($ (bad4)+(-55pt,35pt)+{(4)/2}*(10pt,14pt)$) {$i_0=init$};
%
%
  \draw[forward,->] ($ (bad3)+(-22pt,42pt) $) to($ (bad2)+(-35pt,40pt)+{2/3}*(10pt,10pt) $) node[transitionLabel]{$post(i_1\wedge\phi_2)$};
%
  \draw[forward,->] ($ (bad4)+(-15pt,50pt) $) to ($ (bad3)+(-25pt,50pt)+{1/3}*(10pt,10pt) $)  node[transitionLabel]{$post(i_0 \wedge \phi_3)$};
%
  \draw[forward,->] ($ (bad2)+(-20pt,40pt) $) to ($ (bad1)+(-40pt,30pt)+(10pt,10pt) $) node[transitionLabel] {$post(i_2\wedge\phi_1)$};
\end{tikzpicture}
\end{center}
\label{fig:cegar}
\caption{Counter Example Guided Abstractuion Refinement Scheme for Councurrent Parameterized Systems}
\end{figure*}   


